core_1_summary 9,38
Display forms for primitive terms of type-theory. Abstractions for 
propositions-as-types correspondence. Parenthesization control. 

origin